\section{Conclusions}

\begin{itemize}
	\item Impact of Hash on performance
	\item Impact of encoding of qualified existential quantification
	\item Unnecessary (?) factoring in \quonto
	\item Impact of factoring in \quonto
	\item Necessity of clause containment optimization
	\item Impact on performance with clause containment optimization
\end{itemize}	